The Runtime Complexity (innermost) of the given CpxTRS could be proven to be BOUNDS(n^1, INF).

(0) Obligation:

Runtime Complexity TRS:
The TRS R consists of the following rules:

division(x, y) → div(x, y, 0)
div(x, y, z) → if(lt(x, y), x, y, inc(z))
if(true, x, y, z) → z
if(false, x, s(y), z) → div(minus(x, s(y)), s(y), z)
minus(x, 0) → x
minus(s(x), s(y)) → minus(x, y)
lt(x, 0) → false
lt(0, s(y)) → true
lt(s(x), s(y)) → lt(x, y)
inc(0) → s(0)
inc(s(x)) → s(inc(x))

Rewrite Strategy: INNERMOST

(1) DecreasingLoopProof (EQUIVALENT transformation)

The following loop(s) give(s) rise to the lower bound Ω(n¹):
The rewrite sequence
if(false, s(s(x106208_1)), s(0), z) →⁺ if(false, s(x106208_1), s(0), inc(z))
gives rise to a decreasing loop by considering the right hand sides subterm at position [].
The pumping substitution is [x106208_1 / s(x106208_1)].
The result substitution is [z / inc(z)].

(2) BOUNDS(n^1, INF)